/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package simhya.modelchecking.mtl;
import simhya.model.store.Store;
import simhya.matheval.SymbolArray;
import java.util.HashMap;
import java.util.ArrayList;

/**
 *
 * @author Luca
 */
public abstract class MTLnode {
    MTLnode left; //for binary nodes
    MTLnode right; //for binary nodes
    MTLnode child; //for unary nodes
    MTLnode parent; //parent node
    
    boolean isTopNode;
    boolean isExplorableTopNode;
    boolean [] truthValue;
    int traceLength;
    
    boolean init = false;

    public MTLnode() {
        this.child = null;
        this.left = null;
        this.right = null;
        this.parent = null;
    }
    
    public void setChildren(MTLnode left, MTLnode right) {
        this.left = left;
        this.right = right;
        this.child = null;
    }
    
    public void setChild(MTLnode child) {
        this.child = child;
        this.left = null;
        this.right = null;
    }
    
    public void setParent(MTLnode parent) {
        this.parent = parent;
    }
    
    public void initalize(Store store, SymbolArray localSymbols, HashMap predicatesToExpression) {
        if (left != null) 
            left.initalize(store,localSymbols,predicatesToExpression);
        if (right != null)
            right.initalize(store,localSymbols,predicatesToExpression);
        if (child != null)
            child.initalize(store,localSymbols,predicatesToExpression);
    }
    
    public void recomputeBounds(SymbolArray localSymbols) {
        if (left != null) 
            left.recomputeBounds(localSymbols);
        if (right != null)
            right.recomputeBounds(localSymbols);
        if (child != null)
            child.recomputeBounds(localSymbols);
    }
    
    
    public String toFormulaTree(int depth) {
        String s = "";
        if (left != null) 
            s += left.toFormulaTree(depth+1);
        if (right != null)
            s += right.toFormulaTree(depth+1);
        if (child != null)
            s += child.toFormulaTree(depth+1);
        return s;
    }
    
    /**
     * This functions sets the boolean flag for top nodes
     */
    void setTopNodeInfo() {
        this.setTopNodeInfo(false);
    }
    
    void setTopNodeInfo(boolean belowModelNode) {
        isTopNode = !belowModelNode;
        if (left != null) 
            left.setTopNodeInfo(belowModelNode);
        if (right != null)
            right.setTopNodeInfo(belowModelNode);
        if (child != null)
            child.setTopNodeInfo(belowModelNode);
    }
    
    /**
     * This function checks if the formula has explorable top nodes, 
     * according to the given parameter, and sets the corresponding flag.
     * It requires that the top node information is set.
     * @param parameter  a string for a parameter to explore, or null if one wants 
     * to compare current bounds (check is done on parametricInterval and is syntactic: 
     * all parameters have to coincide, not just their value).
     * 
     */
    void testAndSetExplorableTopNodes(String parameter) {
        ParametricInterval pint = this.setExplorableTopNodes(parameter);
        if (pint != null)
            this.setExplorableTopNodes(parameter, true);
        else this.setExplorableTopNodes(parameter, false);
    }
    
    /**
     * This recursively checks that top intervals of modal operators
     * are compatible for exploration. Returns null if they are not, 
     * the top interval that can be explored if they are compatible
     * @param parameter
     * @return 
     */
    ParametricInterval setExplorableTopNodes(String parameter) {
        return null;
    }
    
    /**
     * This recursively sets the explorableTopNode flag, which is true for all nodes 
     * which can contain a set of points as output, depending on the topmost metric intervals
     * @param parameter
     * @param value 
     */
    void setExplorableTopNodes(String parameter, boolean value) {
        if (this.isTopNode) {
            boolean loc = false;
            if (left != null) {
                left.setExplorableTopNodes(parameter, value);
                loc = loc || left.isExplorableTopNode;
            }
            if (right != null) {
                right.setExplorableTopNodes(parameter, value);
                loc = loc || right.isExplorableTopNode;
            }
            if (child != null) {
                child.setExplorableTopNodes(parameter, value);
                loc = loc || child.isExplorableTopNode;
            }
            this.isExplorableTopNode = value;
        }
    }
            
            
    //replace void with an output data structure,
    boolean[] modelCheck(double [] deltaTimes, boolean varyInterval, boolean varyRightBound, int points) {
        if (!init) 
            throw new RuntimeException("Formula not initialized for model checking");
        this.recursiveLabelingPointwiseSemantics(deltaTimes, varyInterval, varyRightBound, points);       
        init = false;
        return this.truthValue;
    }
    
    //pass suitable parameters
    void initForModelChecking(int points, int traceLength) {
        this.traceLength = traceLength;
        if (!this.isTopNode)
            this.truthValue = new boolean[traceLength];
        else {
            if (this.isExplorableTopNode)
                this.truthValue = new boolean[points];
            else 
                this.truthValue = new boolean[1];
        }
        init = true;
    }
    
    
    
    
    
    
    /**
     * recursively labels the nodes of the formula with the truth values.
     */
    void recursiveLabelingPointwiseSemantics(double [] deltaTimes, 
            boolean varyInterval, boolean varyRightBound, int points) {
        if (left != null)
            left.recursiveLabelingPointwiseSemantics(deltaTimes,varyInterval,varyRightBound,points);
        if (right!=null)
            right.recursiveLabelingPointwiseSemantics(deltaTimes,varyInterval,varyRightBound,points);
        if (child != null)
            child.recursiveLabelingPointwiseSemantics(deltaTimes,varyInterval,varyRightBound,points);
        if (isTopNode)
            this.labelingTopFormulaPointwiseSemantics(deltaTimes,varyInterval && isExplorableTopNode, //labels parametrically the top node only if it is explorable. 
                    varyRightBound,points);
        else
            this.labelingFormulaPointwiseSemantics(deltaTimes);
    }
    
    abstract void labelingTopFormulaPointwiseSemantics(double [] deltaTimes,  
            boolean varyInterval, boolean varyRightBound, int points);
    /**
     * Labels a non-top formula. 
     * @param deltaTimes is the array containing the time deifference between any state
     */
    abstract void labelingFormulaPointwiseSemantics(double [] deltaTimes);
    
    
    
    void collectAtomicNodes(ArrayList<MTLatom> list) {
        if (left != null)
            left.collectAtomicNodes(list);
        if (right != null)
            right.collectAtomicNodes(list);
        if (child != null)
            child.collectAtomicNodes(list);
    }
    
}
